Termination w.r.t. Q proof of TRS/higher-order/AotoYam012.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))

Q is empty.